%
% Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
%
% SPDX-License-Identifier: CC-BY-SA-4.0
%

\documentclass[11pt,a4paper]{article}

\usepackage{isabelle,isabellesym}
\usepackage{changepage}
\usepackage{xcolor}
\usepackage{mdframed}
\usepackage{microtype}
\usepackage[numbers]{natbib}

\definecolor{spot}{rgb}{0,0.2,0.6}

\usepackage{listings}
\definecolor{grey}{rgb}{0.9,0.9,0.9}
\lstset{%
    language=C,
    basicstyle=\small\sffamily,
    columns=fullflexible,
    showstringspaces=false,
    xleftmargin=24pt,
    xrightmargin=24pt
    }

% this should be the last package used
\usepackage{pdfsetup}

% urls in roman style, theory text in math-similar italics
\urlstyle{rm}
\isabellestyle{it}

% for uniform font size
%\renewcommand{\isastyle}{\isastyleminor}

\renewenvironment{isabellebody}{%
    \isamarkuptrue\par%
    \isaspacing\isastyle%
}{%
    \par%
}

\renewenvironment{isabelle}{%
    \medskip%
    \begin{adjustwidth}{1em}{0pt}%
    \begin{mdframed}[%
        leftline=true,rightline=false,topline=false,bottomline=false,%
        linecolor=spot!20,linewidth=2pt,backgroundcolor=spot!3]%
    \begin{trivlist}%
    \begin{isabellebody}%
    \item\relax%
}{%
    \end{isabellebody}%
    \end{trivlist}%
    \end{mdframed}%
    \end{adjustwidth}%
    \medskip%
}


\begin{document}

\title{Getting Started with AutoCorres}
\author{Japheth Lim \and Rohan Jacob-Rao \and David Greenaway}
\maketitle

\tableofcontents
\clearpage

% sane default for proof documents
\parindent 0pt\parskip 0.5ex

% generated text of all theories
\input{session}

% bibliography
\bibliographystyle{plainurl}
\nocite{*}
\bibliography{root}

\end{document}

